COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	fetch intege.ax
C00005 ENDMK
C⊗;
fetch intege.ax;
∧I INDUCTION[P←λK.((M+N)+K=M+(N+K))];
∀E PLUS1 M+N;
∀E PLUS1 N;
TAUTEQ M+N=M+N;
SUBST 3 IN 4 OCC 1;
TAUTEQ 1:#1#2⊃1:#2 1 2 5;
ASSUME 6:#1#1#1;
∀E PLUS2 M+N N1;
SUBSTR 7 IN 8;
∀E PLUS2 M N+N1;
∀E PLUS2 N N1;
SUBST 11 IN 10;
TAUTEQ 6:#1#1#2 12 9;
⊃I 7 13;
∀I 14 N1;
MP 15 6;
∀E 16 K;
∀I 17 M N K;
LABEL ASSOCIATIVITY=18;
AXIOM ONE: 1= SUCC 0;;
∧I INDUCTION[P←λN.(0+N=N)];
∀E PLUS1 0;
TAUT 19:#1#2⊃19:#2 19 20;
ASSUME 21:#1#1#1;
∀E PLUS2 0 N;
SUBSTR 22 IN 23;
⊃I 22 24;
∀I 25 N;
MP 26 21;
LABEL ZEROPLUS = 27;
∧I INDUCTION[P←λM.(M+1 = SUCC M)];
∀E ZEROPLUS 1;
TAUTEQ 28:#1#2⊃28:#2 28 29 ONE;
ASSUME 30:#1#1#1;
TAUTEQ SUCC N +1 = SUCC N +1;
SUBSTR ONE IN 32 OCC 2;
∀E PLUS2 SUCC N 0;
∀E PLUS1 SUCC N;
SUBSTR 35 IN 34;
TAUTEQ 30:#1#2 36 33;
TAUTEQ 30:#1#1#2 36 33;
⊃I 31 37;
∀I 38 N;
MP 39 30;
LABEL PLUSONE 40;
∧I INDUCTION[P←λN.(1+N = SUCC N)];
∀E PLUS1 1;
TAUTEQ 41:#1#2⊃41:#2 41 42 ONE;
ASSUME 43:#1#1#1;
∀E PLUS2 1 N;
SUBSTR 44 IN 45;
⊃I 44 46;
∀I 47 N;
MP 48 43;
LABEL ONEPLUS=49;
∧I INDUCTION[P←λN.(∀M.((M+N)-N = M))];
∀E PLUS1 M;
∀E MINUS2 M+0;
TAUTEQ 52:#1=51:#2 51 52;
∀I 53 M;
TAUT 50:#1#2⊃50:#2 50 54;
ASSUME 55:#1#1#1;
∀E MINUS3 M+SUCC N N;
∀E ONEPLUS N;
SUBST 58 IN 57 OCC 3;
∀E ASSOCIATIVITY M 1 N;
SUBST 60 IN 59;
∀E PLUSONE M;
SUBSTR 62 IN 61;
∀E 56 SUCC M;
SUBSTR 64 IN 63;
∀E PEANO2 M;
SUBSTR 66 IN 65;
∀I 67 M;
⊃I 56 68;
∀I 69 N;
MP 55 70;
∀E 71 N 0;
∀E ZEROPLUS N;
SUBSTR 73 IN 72;
∀I 74 N;